#include "tern/SchedCache.h"
#include "tern/SolverSetting.h"
#include "tern/TernLandmark.h"		// Put it here since both the recording (KLEE) and replaying part need to refer to SchedCache.
#include "tern/TernUtil.h"

using namespace llvm;
using namespace klee;
using namespace klee::expr;
using namespace std;

Char_Ptr_To_Int_Map landmarksMap;			// This is static information, os it is fine to be global.
extern pid_t gettid();

SchedTrunk::SchedTrunk() {
	//trunkIds.clear();
	//trunkInfo.clear();
	trunkSize = 0;
	for (unsigned i = 0; i < SCHED_TRUNK_MAX_SIZE; i++) {
		trunkIds[i] = -1;
		trunkInfo[i] = NULL;
		ops[i] = -1;
	}
	//memset(trunkInfo, 0, sizeof(trunkInfo)*sizeof(const char *));
	cManager = new ConstraintManager();
	prevNode = NULL;
	nextNode = NULL;
	//instId = -1;
	tidFileName = "";
	cstFileName = "";
	enabledTracks.clear();
}

SchedTrunk::~SchedTrunk() {
	// delete cManager;
}

std::string& SchedTrunk::dumpTidsToDisk(unsigned index, int winNum) {
	assert(trunkSize < SCHED_TRUNK_MAX_SIZE);
	int tid = trunkIds[trunkSize - 1];
	char fileName[SMALL_SIZE] = {0};
	unsigned offset = sprintf(fileName, "%s/", DUMP_DIR);
	sprintf(fileName+offset, TRUNK_TID_FILENAME, winNum, index, tid, gettid());
	std::ofstream tidFile(fileName);
	tidFile << trunkSize << "\n";
	for (unsigned i = 0; i < trunkSize; i++) {
		assert(trunkInfo[i]);
		tidFile << trunkInfo[i] << "\n";
	}
	tidFile.flush();
	tidFile.close();

	tidFileName = &(fileName[offset]);
	return tidFileName;
}

void SchedTrunk::loadTidsFromDisk(std::string name) {
	tidFileName = name;
	int tid = -1;
	char fileName[SMALL_SIZE] = {0};
	char tidInfo[BASIC_SIZE] = {0};
	unsigned offset = sprintf(fileName, "%s/", DUMP_DIR);
	sprintf(fileName+offset, "%s", tidFileName.c_str());
	std::ifstream tidFile(fileName);
	unsigned size = 0;

	if (!(tidFile >> size)) {
		fprintf(stderr, "The format of tid file %s is incorrect.\n", tidFileName.c_str());
		exit(1);
	}

	// Read the number, and then read each line of tidInfo.
	tidFile.seekg(0);
	tidFile.getline(tidInfo, sizeof(tidInfo));
	for (unsigned i = 0; i < size; i++) {
		memset(tidInfo, 0, sizeof(tidInfo));
		tidFile.getline(tidInfo, sizeof(tidInfo));
		//rp_dbg("SchedTrunk::loadTidsFromDisk (%s)\n", tidInfo);
		char *newTidInfo = new char[BASIC_SIZE];
		memset(newTidInfo, 0, BASIC_SIZE);
		strcpy(newTidInfo, tidInfo);
		//trunkInfo.push_back(newTidInfo);
		trunkInfo[trunkSize] = newTidInfo;
		tid = atoi(strtok(tidInfo, " "));
		//trunkIds.push_back(tid);
		trunkIds[trunkSize] = tid;
		//rp_dbg("SchedTrunk::loadTidsFromDisk size %u (tid %d)\n", trunkSize, tid);
		ops[trunkSize] = getOpByTidInfo(newTidInfo);
		trunkSize++;
		assert(trunkSize < SCHED_TRUNK_MAX_SIZE);
	}
	tidFile.close();
}

std::string& SchedTrunk::dumpConstraintsToDisk(unsigned index, int winNum) {
	assert(trunkSize < SCHED_TRUNK_MAX_SIZE);
	int tid = trunkIds[trunkSize - 1];
	char fileName[SMALL_SIZE] = {0};
	unsigned offset = sprintf(fileName, "%s/", DUMP_DIR);
	sprintf(fileName+offset, TRUNK_CST_FILENAME, winNum, index, tid, gettid());
	std::ofstream cstFile(fileName);

	// dump symbolic var declarations.
	std::vector<const Array*> objects;
	KeyType key = KeyType(cManager->begin(), cManager->end());
	findSymbolicObjects(key.begin(), key.end(), objects);
	cstFile << "# Number of symbolic variables: " << objects.size() << ".\n\n";
	for (unsigned i = 0; i != objects.size(); ++i) {
		const Array *arr = objects[i];
		cstFile << "array " << arr->name << "[" << arr->size << "] : w8 -> w8 = symbolic" << "\n\n";
	}
	cstFile << "\n\n(query\n";
	cstFile << "[\n";

	// dump expressions.
	cstFile << "# Number of constraints: " << cManager->size() << ".\n\n";
	for (ConstraintManager::constraint_iterator it = cManager->begin(), ie = cManager->end(); it != ie; ++it) {
		ref<Expr> ce = *it;
		ce->print(cstFile);
		cstFile << "\n\n";
	}
	cstFile << "]\n";
	cstFile << "false\n";
	cstFile << "[] [])\n";
	cstFile.flush();
	cstFile.close();

	cstFileName = &(fileName[offset]);
	return cstFileName;
}

void SchedTrunk::loadConstraintsFromDisk(std::string name) {
	string errorStr;
	cstFileName = name;
	char fileName[SMALL_SIZE] = {0};
	unsigned offset = sprintf(fileName, "%s/", DUMP_DIR);
	sprintf(fileName+offset, "%s", cstFileName.c_str());
	//fprintf(stderr, "Loading constraint file (%s)\n", fileName);
	MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(fileName, &errorStr); 
	if (MB == NULL) {
		fprintf(stderr, "Failed to init MemoryBuffer\n");
		exit(1);
	}
	ExprBuilder *Builder = createDefaultExprBuilder();
	if (Builder == NULL) {
		fprintf(stderr, "Failed to init ExprBuilder\n");
		exit(1);
	}
	if (cManager)
		delete cManager;
	cManager = parseConstraints(fileName, MB, Builder);
	if (cManager == NULL) {
		fprintf(stderr, "Failed to parseConstraints\n");
		exit(1);
	}
}

ConstraintManager *SchedTrunk::parseConstraints(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) {
	ConstraintManager *cManager = NULL;
	std::vector<Decl *> Decls;
	Parser *P = Parser::Create(Filename, MB, Builder);
	P->SetMaxErrors(20);
	int i = 0;
	while (Decl *D = P->ParseTopLevelDecl()) {
		Decls.push_back(D);
		if (isa<QueryCommand>(D)) {
			cManager = new ConstraintManager(dyn_cast<QueryCommand>(D)->Constraints);
			my_print( "Num of constraints at initConstraintManager %u\n", dyn_cast<QueryCommand>(D)->Constraints.size());
		} else
			i++;
	}

	bool success = true;
	if (unsigned N = P->GetNumErrors()) {
		std::cerr << Filename << ": parse failure: "
			<< N << " errors.\n";
		success = false;
	}  

	if (!success)
		return NULL;
	return cManager;
}

std::string& SchedTrunk::getTidFileName() {
	return tidFileName;
}

std::string& SchedTrunk::getCstFileName() {
	return cstFileName;
}

/* When using this function, be careful, since it is going to modify the tidInfo string. */
int SchedTrunk::getOpByTidInfo(char *tidInfo) {
	assert(tidInfo);
	// tern_symbolic is special, since the landmark containts symbolic var name, so we return earlier.
	if (strstr(tidInfo, TERN_SYMBOLIC_LANDMARK))
		return landmarksMap[TERN_SYMBOLIC_LANDMARK];
	
	char buf[BASIC_SIZE];
	memset(buf, 0, BASIC_SIZE);
	strcpy(buf, tidInfo);
	char *lmStart = strstr(buf, "{");
	char *lmEnd = strstr(buf, "}");
	lmStart++;
	char tmp = lmEnd[0];
	lmEnd[0] = '\0';
	int result = landmarksMap[lmStart];
	lmEnd[0] = tmp;
	return result;
}

// Still keep the old tid in second column for debug purpose.
void SchedTrunk::updateTidInfoWithNewTid(unsigned index, int newTid) {
	char *newTidInfo = new char[BASIC_SIZE];
	char *tidInfo = tidInfoAt(index);

	//fprintf(stderr, "	SchedTrunk::updateTidInfoWithNewTid old tidInfo %s\n", tidInfo);fflush(stderr);
	assert(newTid >= 0);
	memset(newTidInfo, 0, BASIC_SIZE);
	sprintf(newTidInfo, "%d %d%s", newTid, tidAt(index), strstr(tidInfo, " "));
	setTidAt(index, newTid);
	setTidInfoAt(index, newTidInfo);
	delete tidInfo;
	//fprintf(stderr, "	SchedTrunk::updateTidInfoWithNewTid new tidInfo %s\n", tidInfo);fflush(stderr);
}

unsigned SchedTrunk::size() {
	assert(trunkSize < SCHED_TRUNK_MAX_SIZE);
	return trunkSize;
}

SchedNode *SchedTrunk::getPrevNode() {
	return prevNode;
}

void SchedTrunk::setPrevNode(SchedNode *node) {
	prevNode = node;
}

SchedNode *SchedTrunk::getNextNode() {
	return nextNode;
}

void SchedTrunk::setNextNode(SchedNode *node) {
	nextNode = node;
	nextNode->setPrevTrunk(this);
}

int SchedTrunk::tidAt(unsigned index) {
	return trunkIds[index];
}

int SchedTrunk::setTidAt(unsigned index, int newTid) {
	return trunkIds[index] = newTid;
}

char *SchedTrunk::tidInfoAt(unsigned index) {
	return trunkInfo[index];
}

void SchedTrunk::setTidInfoAt(unsigned index, char *newTidInfo) {
	trunkInfo[index] = newTidInfo;
}

int SchedTrunk::opAt(unsigned index) {
	return ops[index];
}

ConstraintManager *SchedTrunk::getCst() {
	return cManager;
}

std::vector<const Array*> &SchedTrunk::getObjects() {
	return objects;
}

Char_Ptr_To_Int_Map &SchedTrunk::getCache() {
	return cache;
}

// Temporarily just leaves trackId useless.
unsigned SchedTrunk::constraintSize(unsigned trackId) {
	assert(trackId < TASK_WINDOW_SIZE);
	return cManager->size();
}

int SchedTrunk::addTid(char *tidInfo) {
	int tid = -1;
	char buf[BASIC_SIZE];
	
	assert(tidInfo != NULL);
	trunkInfo[trunkSize] = tidInfo;
	memset(buf, 0, BASIC_SIZE);
	strcpy(buf, tidInfo);
	tid = atoi(strtok(buf, " "));
	trunkIds[trunkSize] = tid;
	ops[trunkSize] = getOpByTidInfo(tidInfo);	
	trunkSize++;
	assert(trunkSize < SCHED_TRUNK_MAX_SIZE);
	
	return 0;
}

int SchedTrunk::addConstraint(unsigned trackId, ref<Expr> expr) {
	assert(trackId < TASK_WINDOW_SIZE);
	cManager->addConstraint(expr);
	return 0;
}

void SchedTrunk::addSymVar(const Array *arr) {
	for (unsigned i = 0; i < objects.size(); i++) {
		if (objects[i]->name == arr->name) {
			fprintf(stderr, "WARN: SchedTrunk::addSymVar\n");
			return;
		}
	}
	objects.push_back(arr);
}

bool SchedTrunk::isLeafTrunk() {
	return (ops[trunkSize-1] == END_TASK_LANDMARK_IDX);	
}

void SchedTrunk::addEnabledTrack(unsigned trackIdx) {
	//assert(enabledTracks.find(trackIdx) == enabledTracks.end());
	for (unsigned i = 0; i < enabledTracks.size(); i++) {
		assert(enabledTracks[i] != trackIdx);
	}
	enabledTracks.push_back(trackIdx);
}

std::vector<unsigned> &SchedTrunk::getEnabledTracks() {
	return enabledTracks;
}

SchedNode::SchedNode() {
	children.clear();
	prevTrunk = NULL;
}

void SchedNode::addChild(SchedTrunk *schedTrunk) {
	//fprintf(stderr, "SchedNode::addChild %p, %p\n", (void *)this, (void *)schedTrunk);
	children.push_back(schedTrunk);
	schedTrunk->setPrevNode(this);
}

void SchedNode::delChild(unsigned index) {
	children.erase(children.begin()+index);
}

SchedTrunk *SchedNode::getChild(unsigned index) {
	assert(index < children.size());
	return children[index];
}

SchedTrunk *SchedNode::getPrevTrunk() {
	return prevTrunk;
}
void SchedNode::setPrevTrunk(SchedTrunk *st) {
	prevTrunk = st;
	if (st->getNextNode() == NULL) {
		sc_print( "WARN: SchedNode::setPrevTrunk setNextNode %p\n", (void *)this);
		st->setNextNode(this);
	}
}

unsigned SchedNode::size() {
	/*for (unsigned i = 0; i < children.size(); i++) {
		fprintf(stderr, "Node %p: child trunk %s\n", (void *)this, getChild(i)->getTidFileName().c_str());
	}*/
	return children.size();
}

MemoizedSched::MemoizedSched() {
	schedTrunks.clear();
}

void MemoizedSched::dumpSchedTrunksToDisk(int winNum) {
 	const char *surfix = "orig_sched";
	char schedInfo[LONG_SIZE];
	unsigned offset = 0;
	int numInput = 0;
	std::string tmp = "";
	char inputItem[BASIC_SIZE] = {0};
	char linearFile[BASIC_SIZE] = {0};
	char tmpFile[BASIC_SIZE] = {0};

	memset(inputItem, 0, BASIC_SIZE);
	memset(linearFile, 0, BASIC_SIZE);
	memset(tmpFile, 0, BASIC_SIZE);
 	sprintf(linearFile, "%s.%s", INPUT, surfix);
	sprintf(tmpFile, "%s.%s.tmp", INPUT, surfix);
 	std::ifstream oldInput(linearFile);
 	std::ofstream newInput(tmpFile);

 	memset(schedInfo, 0, LONG_SIZE);
	offset += sprintf(schedInfo, "%u || ", (unsigned)schedTrunks.size());
	for (unsigned i = 0; i < schedTrunks.size(); i++) {
 		tmp = schedTrunks[i]->dumpTidsToDisk(i, winNum);
		offset += sprintf(schedInfo + offset, "%s ", tmp.c_str());
		tmp = schedTrunks[i]->dumpConstraintsToDisk(i, winNum);
		offset += sprintf(schedInfo + offset, "%s || ", tmp.c_str());
		assert(offset < LONG_SIZE);
 	}

 	// Update ece.input.orig_sched.
	if (oldInput.is_open()) {
		if (!(oldInput >> numInput)) {
			fprintf(stderr, "ORDER module failed to read %s\n", INPUT);
			exit(1);
		}
		oldInput.seekg(0);
		oldInput.getline(inputItem, sizeof(inputItem));
	}
	numInput++;

	newInput << numInput << " \n";
	newInput << schedInfo << "\n";	// Heming: new added schedule will be matched first.
	for (int i = 0; i < numInput - 1; i++) {
		memset(inputItem, 0, sizeof(inputItem));
		oldInput.getline(inputItem, sizeof(inputItem));
		newInput << inputItem << "\n";
	}	
	oldInput.close();
	newInput.flush();
	newInput.close();
	rename(tmpFile, linearFile); 
}

SchedTrunk *MemoizedSched::getTrunk(unsigned index) {
	assert(index < schedTrunks.size());
	return schedTrunks[index];
}

unsigned MemoizedSched::size() {
	return schedTrunks.size();
}

int MemoizedSched::addTid(char *tidInfo) {
	// add tidInfo to current schedTrunk.
	// If it is tern_symbolic, then create a new trunk.
	// This function only interacs with class MemoizedSchedule (a layered approach).
	if (schedTrunks.size() == 0 && (strstr(tidInfo, START_TASK_LANDMARK))) {		// The first tern_symbolic always come with the taskStart.
		SchedTrunk *newTrunk = new SchedTrunk();
		schedTrunks.push_back(newTrunk);
		fprintf(stderr, "MemoizedSched::addTid START_TASK_LANDMARK created new trunk %u\n", (unsigned)schedTrunks.size());
	}
	
	assert(schedTrunks.size() > 0);
	int result = schedTrunks[schedTrunks.size()-1]->addTid(tidInfo);

	// If we meet a tern_symbolic landmark, then we meet the end of the current trunk.
 	if (strstr(tidInfo, TERN_SYMBOLIC_LANDMARK) && schedTrunks.size() > 0) {
		SchedTrunk *newTrunk = new SchedTrunk();
		schedTrunks.push_back(newTrunk);
		fprintf(stderr, "MemoizedSched::addTid TERN_SYMBOLIC_LANDMARK created new trunk %u\n", (unsigned)schedTrunks.size());
	}

	return result;
}

int MemoizedSched::addConstraint(unsigned trackId, ref<Expr> expr) {
	// add tidInfo to current schedTrunk.
	assert(schedTrunks.size() > 0);
	return schedTrunks[schedTrunks.size()-1]->addConstraint(trackId, expr);
}

void MemoizedSched::addSymVar(const Array *arr) {
	assert(schedTrunks.size() > 0);
	return schedTrunks[schedTrunks.size()-1]->addSymVar(arr);
}

// Normalize the Tid of each op, let them start from 1.
void MemoizedSched::normalize() {
	Int_To_Int_Map tidMap;
	tidMap.clear();
	int cnt = 1;

	for (unsigned i = 0; i < size(); i++) {
		SchedTrunk *sTrunk = getTrunk(i);
		for (unsigned j = 0; j < sTrunk->size(); j++) {
			int oldTid = sTrunk->tidAt(j);
			if (tidMap.find(oldTid) == tidMap.end()) {
				tidMap[oldTid] = cnt;
				cnt++;
			}
			sTrunk->updateTidInfoWithNewTid(j, tidMap[oldTid]);
		}
	}
}

SchedTrack::SchedTrack(const char *id, const char *kw, unsigned idx) {
	schedId = id;
	keyWord = "sqlcmd";					// For mysqld only, so far.
	index = idx;
	trunks.clear();
	trackManager = std::vector< std::vector<ConstraintManager *> >(TASK_WINDOW_SIZE);
	trackObjects = std::vector< std::vector<const Array*> >(TASK_WINDOW_SIZE);
	replayTidWaitQueue = std::vector< std::vector<int> >(TASK_WINDOW_SIZE);
}

void SchedTrack::addCManager(unsigned trackId, ConstraintManager *cm) {
	trackManager[trackId].push_back(cm);
}

unsigned SchedTrack::getBackCManagerSize(unsigned trackId) {
	return trackManager[trackId].back()->size();
}

void SchedTrack::addObj(unsigned trackId, const Array *arr) {
	trackObjects[trackId].push_back(arr);
}
		
void SchedTrack::addConstraint(unsigned trackId, ref <Expr> expr) {
	trackManager[trackId].back()->addConstraint(expr);
}

std::vector<ConstraintManager *> &SchedTrack::getCsts(unsigned trackId) {
	return trackManager[trackId];
}

std::vector<const Array *> &SchedTrack::getObjs(unsigned trackId) {
	return trackObjects[trackId];
}

void SchedTrack::buildTrack(SchedTrunk *cT, SchedNode *root) {
	SchedTrunk *curTrunk = cT;
	SchedNode *curNode = curTrunk->getPrevNode();
	assert(curTrunk && curNode);
	ConstraintManager *curCst = curTrunk->getCst();
	trunks.insert(trunks.begin(), curTrunk);

	std::vector< char *> symVarNames = std::vector< char *>(TASK_WINDOW_SIZE);
	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		symVarNames[i] = new char[TINY_SIZE];
		memset(symVarNames[i], 0, TINY_SIZE);
		sprintf(symVarNames[i], "%s%u", keyWord, i+1);
	}

	// For each trunk in this schedule.
	do {
		// Each trunk in a schedule corresponds a cst manager in the this track.
		for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
			ConstraintManager *cm = new ConstraintManager();
			addCManager(i, cm);
		}

		std::vector< const Array * > arr = std::vector< const Array * >(TASK_WINDOW_SIZE);
		for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
			arr[i] = NULL;
		}
		
		for (ConstraintManager::const_iterator it = curCst->begin(), ie = curCst->end(); it != ie; ++it) {
			ref <Expr> expr = *it;
			std::vector<const Array*> objects;
			objects.clear();
			findSymbolicObjects(expr, objects);
			
			// If we have more than one symbolic variables in one expression, then just ignore this expression.
			assert(objects.size() > 0);
			if (objects.size() > 1)
				continue;

			for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
				if (strcmp(objects[0]->name.c_str(), symVarNames[i]) == 0) {
					addConstraint(i, expr);			
					if (arr[i] == NULL) {
						arr[i] = objects[0];
					}
				}
			}			
		}

		// Some arr may be NULL, but this is fine, since the cManager is also empty.
		for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
			addObj(i, arr[i]);
			// For debug.
			/*fprintf(stderr, "SchedTrack[%u] at %s: trunk %s built, cst size %u, arr obj %p\n", 
				i, schedId, curTrunk->getTidFileName().c_str(), getBackCManagerSize(i), (void *)arr[i]);*/
		}

		// If hit the root, then this schedule has been finished to built.
		if (curNode == root)
			break;

		// Backtrack from leav to the root of the sched cache.
		curTrunk = curNode->getPrevTrunk();	
		trunks.insert(trunks.begin(), curTrunk);
		curTrunk->addEnabledTrack(index);
		curNode = curTrunk->getPrevNode();
		assert(curTrunk && curNode);
		curCst = curTrunk->getCst();
	} while (1);

	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		delete symVarNames[i];
	}
	symVarNames.clear();

	/*fprintf(stderr, "SchedTrack %s has been built, size %u, trunks:\n", schedId, getCsts(0).size());
	for (unsigned i = 0; i < trunks.size(); i++) {
		fprintf(stderr, "Trunk[%u]: %s\n", i, trunks[i]->getTidFileName().c_str());
	}
	fprintf(stderr, "\n\n\n");*/
}

bool SchedTrack::checkTrackAt(unsigned trackId, std::vector< std::vector<unsigned char> > &values, int checkerReplayTid) {
	if (!IS_MYSQLD)
		return true;

	// Check the constraints of this track.
	std::vector<ConstraintManager *> cms = getCsts(trackId);
	std::vector<const Array *> objs = getObjs(trackId);
	assert(cms.size() == objs.size());
	std::vector<const Array*> objectsForBinding;
	for (unsigned i = 0; i < cms.size(); i++) {
		//fprintf(stderr, "SchedTrack::checkTrackAt %p %p %u\n", (void *)cms[i], (void *)objs[i], i);
		if (cms[i]->size() == 0)
			continue;

		//assert(objs[i]);
		objectsForBinding.clear();
		KeyType key = KeyType(cms[i]->begin(), cms[i]->end());
		findSymbolicObjects(key.begin(), key.end(), objectsForBinding);
		//objectsForBinding.push_back(objs[i]);
		Assignment binding(objectsForBinding, values);
		assert(objectsForBinding.size() == 1);
		/*fprintf(stderr, "SchedTrack::checkTrackAt %s file, %p %p %u binding %u %u\n", 
			schedId, (void *)cms[i], (void *)objs[i], i, objectsForBinding[0]->size, values[0].size());fflush(stderr);
		fprintf(stderr, "cm size %u, obj name %s\n", 
			cms[i]->size(), objs[i]->name.c_str());
		for (ConstraintManager::constraint_iterator it = cms[i]->begin(), ie = cms[i]->end(); it != ie; ++it) {
			ref<Expr> expr = *it;
			expr->print(std::cerr);
			fprintf(stderr, "\n\n\n");
			fflush(stderr);
		}*/
		// Must satisfy the expressions of this symbolic var in all trunks.
		if (!binding.satisfies(cms[i]->begin(), cms[i]->end())) {
			/*fprintf(stderr, "TID %d MYTID %d, trackID %u, SchedTrack::checkTrack %s the %u th cst (total %u trunks) does not match!\n",
				gettid(), checkerReplayTid, trackId, schedId, i, cms.size());
			for (unsigned j = 0; j < values[0].size(); j++) {
				fprintf(stderr, "%d, ", (int)values[0][j]);
			}
			fprintf(stderr, "\n\n\n");
			fflush(stderr);*/
			return false;
		} else {
			/*fprintf(stderr, "TID %d MYTID %d, trackID %u, SchedTrack::checkTrack %s the %u th cst (total %u trunks) MATCH!\n",
				gettid(), checkerReplayTid, trackId, schedId, i, cms.size());
			for (unsigned j = 0; j < values[0].size(); j++) {
				fprintf(stderr, "%d, ", (int)values[0][j]);
			}
			fprintf(stderr, "\n\n\n");
			fflush(stderr);*/
		}
	}

	/*fprintf(stderr, "TID %d MYTID %d, trackID %u, SchedTrack::checkTrack MATCH schedule %s, emptyNum %u!\n",
		gettid(), checkerReplayTid, trackId, schedId, emptyNum());*/

	return true;
}

const char *SchedTrack::getTrackId() {
	return schedId;
}

void SchedTrack::insertReplayTidAt(unsigned trackId, int replayTid) {
	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		for (unsigned j = 0; j < replayTidWaitQueue[i].size(); j++) {
			if (replayTidWaitQueue[i].at(j) == replayTid) {
				replayTidWaitQueue[i].erase(replayTidWaitQueue[i].begin()+j);
				break;
			}
		}

		for (unsigned j = 0; j < replayTidWaitQueue[i].size(); j++) {
			if (replayTidWaitQueue[i].at(j) == replayTid) {
				replayTidWaitQueue[i].erase(replayTidWaitQueue[i].begin()+j);
				break;
			}
		}
	}
	replayTidWaitQueue[trackId].push_back(replayTid);
}

bool SchedTrack::isFull() {
	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		if (replayTidWaitQueue[i].size() == 0)
			return false;
	}
	return true;
}

bool SchedTrack::isEmptyAt(unsigned trackId) {
	if (replayTidWaitQueue[trackId].size() == 0)
		return true;
	return false;
}

unsigned SchedTrack::emptyNum() {
	unsigned cnt = 0;
	
	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		if (replayTidWaitQueue[i].size() == 0)
			cnt++;
	}
	return cnt;
}

int SchedTrack::start(unsigned trackId) {
	assert(replayTidWaitQueue[trackId].size() > 0);
	int tid = replayTidWaitQueue[trackId].at(0);
	replayTidWaitQueue[trackId].erase(replayTidWaitQueue[trackId].begin());
	return tid;
}

void SchedTrack::delTid(int replayTid) {
	for (unsigned i = 0; i < TASK_WINDOW_SIZE; i++) {
		for (unsigned j = 0; j < replayTidWaitQueue[i].size(); j++) {
			if (replayTid == replayTidWaitQueue[i].at(j)) {
				replayTidWaitQueue[i].erase(replayTidWaitQueue[i].begin()+j);
				break;
			}
		}
	}
}

unsigned SchedTrack::getIndex() {
	return index;
}

SchedTrunk *SchedTrack::getTrunkAt(unsigned i) {
	assert(trunks.size() > i);
	return trunks[i];
}


CacheItr::CacheItr() {
	init();
}

void CacheItr::init() {
	rp_dbg("CacheItr::init\n");
	curNode = NULL;
	// While flushing the cache itr, this is the main flag to indicate whether the flushing work has finished. This function will be called by markBroken() in replayer.
	curTrunk = NULL;
	offset = 0;
	move = 0;
	hTplTid = -1;
	curSchedTrackIdx = -1;
	trackTrunkOffset = 0;
	memset(tidMap, -1, MAX_THREAD_NUM*sizeof(int));
	memset(reversedTidMap, -1, MAX_THREAD_NUM*sizeof(int));
	symVarValueMap.clear();
	rp_dbg("CacheItr::init symVarValueMap return\n");
	//gettimeofday(&tInit, NULL);
}

int CacheItr::getOffset() {
	return offset;
}

unsigned CacheItr::getMove() {
	return move;
}

SchedTrunk *CacheItr::getCurTrunk() {
	return curTrunk;
}

void CacheItr::setCurTrunk(SchedTrunk *st) {
	sc_print( "CacheItr::setCurTrunk %p\n", (void *)st);
	curTrunk = st;
	if (curTrunk)
		hTplTid = curTrunk->tidAt(0);
}

SchedNode *CacheItr::getCurNode() {
	return curNode;
}

void CacheItr::setCurNode(SchedNode *sn) {
	curNode = sn;
}

bool CacheItr::myTurn(unsigned arg, int templateTid, int hookId) {
	if (hTplTid == templateTid) {
		// COMPARE HOOK ID (CALLSITE) AS WELL?
		if (curTrunk->opAt(offset) != (int)arg) {
			rp_dbg("OPMISMATCH1: TID %d MYTID (template) %d CacheItr::myTurn offset %d, move %u, arg %u(%s), tidInfo %s.\n", 
				gettid(), templateTid, offset, move, arg, landmarks[arg], curTrunk->tidInfoAt(offset));
			return false;
			//assert(false);
		}
		//fprintf(stderr, "myTurn RETURN TRUE, TID %d, arg %u CacheItr::myTurn offset %u, move %u\n", tid, arg, getOffset(), getMove());
		return true;
	}
	else {
		//fprintf(stderr, "myTurn RETURN FALSE, TID %d, arg %u CacheItr::myTurn offset %u, move %u\n", tid, arg, getOffset(), getMove());
		return false;
	}
}

// If return value >= 0, means valid tid.
// If return value == -1, means invalid tid. NULL trunk.
// If return value == -2, means finish schedule.
// If return value == -3, means next is start_task, but we do not known the mapping yet (unknown).
MoveOnRet CacheItr::moveOn(int tid, int hookId, unsigned arg, int &nextTid) {
	//fprintf(stderr, "CacheItr::moveOn arg %s\n", landmarks[arg]);
	if (curTrunk == NULL)
		return UnKnown;
	if (offset < (int)curTrunk->size()) {
		// Not only checking the tid, but also checking the landmark type.
		if (curTrunk->opAt(offset) != (int)arg) {
			rp_dbg("OPMISMATCH2: TID %d CacheItr::moveOn arg %u(%s), tidInfo %s.\n", gettid(), arg, landmarks[arg], curTrunk->tidInfoAt(offset));
			return OpMisMatch;
		}
		if (REPLAYER_CHECK_HOOK_ID) {
			char hookInfo[TINY_SIZE];
			memset(hookInfo, 0, TINY_SIZE);
			sprintf(hookInfo, "hook-%d", hookId);
			if (!strstr(curTrunk->tidInfoAt(offset), hookInfo)) {
				rp_dbg("OPMISMATCH HOOK MIS: TID %d CacheItr::moveOn arg %u(%s), tidInfo %s, curHookInfo %s.\n", 
					gettid(), arg, landmarks[arg], curTrunk->tidInfoAt(offset), hookInfo);
			}
		}
		move++;

		/* offset is the most important flag, must update it last. 
		     This if ... else ... is to avoid race and make this basicblock and the if (offset == -1) branch below to be atomic.
		  */
		if (offset + 1 == (int)curTrunk->size()) {
			hTplTid = -1;					// Must update hTplTid before updating offset to avoid race.
			offset = -1;
		}
		else {
			offset++;
			hTplTid = curTrunk->tidAt(offset);
		}

		/*gettimeofday(&tNow, NULL);
		long interval = (tNow.tv_sec - tInit.tv_sec)*1000000 + (tNow.tv_usec - tInit.tv_usec);*/
		rp_dbg("CacheItr::moveOn() hookId %d, offset %d, move %u, curTrunk %s, TID %d MYTID %d arg %u(%s).\n", 
			hookId, offset, move, curTrunk->getTidFileName().c_str(), gettid(), tid, arg, landmarks[arg]);
	}
	if (offset == -1) {
		const char *trunkName = curTrunk->getTidFileName().c_str();
		curNode = curTrunk->getNextNode();			// Move to next node of current trunk.
		curTrunk = NULL;											// Wait for the next tern_symbolic call to update this field.
		offset = 0;
		//fprintf(stderr, "CacheItr::moveOn set curTrunk to NULL because current trunk is used completely\n");
		if (curNode == NULL) {
			if (PRINT_FINISH_SCHED_INFO) {
				fprintf(stderr, HIGHLIGHT_STR_BEFORE);
				fprintf(stderr, "FINISH SCHEDULE with move %u, trunk %s\n", move, trunkName);
				fprintf(stderr, HIGHLIGHT_STR_AFTER);
				fflush(stderr);
			}
			return SchedFinish;
		}
		return UnKnown;
	}
	else if (curTrunk->opAt(offset) == START_TASK_LANDMARK_IDX)
		return TaskStart;
	else {
		int tid = getReversedTidMap(hTplTid);
		sc_print( "CacheItr::moveOn return with tid %d\n", tid);
		nextTid = tid;
		return OK;
	}
}

void CacheItr::setTidMap(int replayerTid, int templateTid) {
	assert(replayerTid >= 0 && templateTid >= 0);
	if (IS_BATCH_PROGRAM) {
		// For batch program, the replayer tid must be the same as template tid,
		// since batch program is deterministic completely.
		if (replayerTid != templateTid) {
			fprintf(stderr, "CacheItr::setTidMap, batch, fail %d %d\n", replayerTid, templateTid);
			assert(false);
		}
	}
	tidMap[replayerTid] = templateTid;
	reversedTidMap[templateTid] = replayerTid;
	my_print( "TID %d CacheItr::setTidMap MAP replayerTid %d, templateTid %d \n", gettid(), replayerTid,  templateTid);
}

int CacheItr::getTidMap(int replayerTid) {
	if (IS_BATCH_PROGRAM) {
		return replayerTid;
	}
	return tidMap[replayerTid];
}

int CacheItr::getReversedTidMap(int templateTid) {
	if (IS_BATCH_PROGRAM) {
		return templateTid;
	}
	return reversedTidMap[templateTid];
}

void CacheItr::moveItrToNextTrunk(int replayTid, SchedTrunk * nextTrunk) {
	setCurNode(nextTrunk->getNextNode());
	setCurTrunk(nextTrunk);									// Update offset and curTrunk at last to avoid race.
}

char *CacheItr::fillSymVarMap(const char *name, void *addr, unsigned nBytes) {
	char *newValue = new char[nBytes+1];
	memset(newValue, 0, nBytes+1);
	for (unsigned i = 0; i < nBytes; i++) {
		newValue[i] = (char)(*((long *)((long)addr + i)));
	}
	assert(symVarValueMap.find(name) == symVarValueMap.end());
	rp_dbg("SchedCache::satisfy insert name %s to symVarValueMap value %s\n", name, newValue);
	symVarValueMap[name] = newValue;
	return newValue;
}

void CacheItr::initSchedTrack(unsigned idx, SchedTrunk *cT) {
	curSchedTrackIdx = idx;
	curTrunk = cT;
	curNode = cT->getPrevNode();
	offset = 0;
	move = 0;
	trackTrunkOffset = 0;
}

unsigned CacheItr::moveOnSchedTrackTrunk() {
	trackTrunkOffset++;
	return trackTrunkOffset;
}

SchedCache::SchedCache() {
	schedNum = 0;
	schedules.clear();
	root = NULL;
	itr = root;
	tracks.clear();
	numTracks = 0;
	initSolver();
	for (unsigned i = 0; i < (sizeof landmarks)/(sizeof landmarks[0]); i++) {
		landmarksMap[landmarks[i]] = (int)i;
	}
}

Solver *SchedCache::constructSolverChain(STPSolver *stpSolver,
                             std::string queryLogPath,
                             std::string stpQueryLogPath,
                             std::string queryPCLogPath,
                             std::string stpQueryPCLogPath) {
  Solver *solver = stpSolver;

//  if (UseSTPQueryPCLog)
//    solver = createPCLoggingSolver(solver, 
//                                   stpQueryLogPath);

//  if (UseFastCexSolver)
//    solver = createFastCexSolver(solver);

//  if (UseCexCache)
    solver = createCexCachingSolver(solver);

//  if (UseCache)
    solver = createCachingSolver(solver);

//  if (UseIndependentSolver)
    solver = createIndependentSolver(solver);

//  if (DebugValidateSolver)
 //   solver = createValidatingSolver(solver, stpSolver);

//  if (UseQueryPCLog)
//    solver = createPCLoggingSolver(solver, 
//                                   queryPCLogPath);
  return solver;
}
 
void SchedCache::initSolver() {
	STPSolver *stpSolver = new STPSolver(false);
	//Solver *solver = 
	solver = 
		constructSolverChain(stpSolver, "tern-queries.qlog", "tern-stp-queries.qlog", "tern-queries.pc", "tern-stp-queries.pc");  
	//tSolver = new TimingSolver(solver, stpSolver);
}

#if 0
// FIXME: if there are more symbolic vars in constraints than in my database + addr, then we should return false.
bool SchedCache::satisfy(CacheItr *cItr, ConstraintManager *cm, std::vector<const Array*> &objects, void *addr, unsigned nbytes, const char *name) {
	//printCst(cm);

	if (cm->size() == 0) {
		fprintf(stderr, "WARN: SchedCache::satisfy, the number of constraints should be greater than 0.\n");
		return true;
	}
	KeyType key = KeyType(cm->begin(), cm->end());
	//std::vector<const Array*> objects;
	std::vector< std::vector<unsigned char> > values;
	if (objects.size() == 0)
		findSymbolicObjects(key.begin(), key.end(), objects);
	assert(objects.size() > 0);
	values = std::vector< std::vector<unsigned char> >(objects.size());		// Each time just checks one symbolic var.

	// Fill in exising values.
	unsigned filledNum = 0;
	int curIndex = -1;
	for (unsigned i = 0; i < objects.size(); i++) {
		bool filled = false;
		for (Sym_Var_To_Value_Map::iterator mapItr = cItr->symVarValueMap.begin(); 
		mapItr != cItr->symVarValueMap.end(); mapItr++) {
			//fprintf(stderr, "SchedCache::satisfy symbolic var name %s %s.\n", mapItr->first, objects[i]->name.c_str());
			if (strcmp(mapItr->first, objects[i]->name.c_str()) == 0) {
				std::vector<unsigned char> &data = values[i];
				data.clear();
				for (unsigned j = 0; j < objects[i]->size; j++) {
					char *value = mapItr->second;
					data.push_back(value[j]);
				}
				filledNum++;
				filled = true;
			}
		}
	}

	// May cover existing value, but this is fine, since this value in addr is the latest one.
	for (unsigned i = 0; i < objects.size(); i++) {
		if (strcmp(name, objects[i]->name.c_str()) == 0) {
			curIndex = (int)i;
			std::vector<unsigned char> &data = values[i];
			data.clear();
			unsigned offset = 0;
			for (unsigned k = 0; k < nbytes; k++) {
				data.push_back((char)(*((long *)((long)addr + offset))));
				//fprintf(stderr, "TERN: SchedCache pushes %u for symbolic var to data offset %u\n", (char)(*((int *)((int)addr + offset))), (unsigned)data.size());
				//fflush(stderr);
				offset += 1;
			}
		}
	}

	// When filling addr for concrete value, we did not inc filledNum, this is for checking.
	// Above is wrong, below is correct: sometimes the queried name may not exist in constraints, like "n" in LU.
	if (curIndex == -1) {
		fprintf(stderr, "SchedCache::satisfy filledNum %u, objects size %u, curIndex %d\n", filledNum, (unsigned)objects.size(), curIndex);
		fflush(stderr);
		return true;
	}

	//Overhead is at the prev part of this function. If put return true here, throughput of httpd is only 4256. If put return true at the top of this function, 10000.
	//return true;
	
	Assignment binding(objects, values);
	//return true;
	if (binding.satisfies(cm->begin(), cm->end())) {
		// If satisfy, then update values in symVarValueMap.
		char *newValue = new char[values[curIndex].size()];
		memset(newValue, 0, values[curIndex].size());
		for (unsigned i = 0; i < values[curIndex].size(); i++) {
			newValue[i] = (char)(values[curIndex][i]);
		}
		my_print( "SchedCache::satisfy insert %s to symVarValueMap\n", name);
		//assert(cItr->symVarValueMap.find(name) == cItr->symVarValueMap.end());			// No duplicate sym var name.
		cItr->symVarValueMap[name] = newValue;
		return true;
	} else {
		return false;
	}
}
#endif

// Note: must call fillSymVarMap() before return true in this function, since "true" imply that the cache itr has accepted the concrete value for next steps.
bool SchedCache::satisfyWithCache(CacheItr *cItr, ConstraintManager *cm, std::vector<const Array*> &objects, 
	Char_Ptr_To_Int_Map &cache, void *addr, unsigned nbytes, const char *name) {
	rp_dbg("SchedCache::satisfyWithCache\n");
	if (cm->size() == 0) {
		rp_dbg("WARN: SchedCache::satisfy, the number of constraints should be greater than 0.\n");
		cItr->fillSymVarMap(name, addr, nbytes);
		return true;
	}
	KeyType key = KeyType(cm->begin(), cm->end());
	std::vector< std::vector<unsigned char> > values;
	fillSymObjs(key, objects);
	assert(objects.size() > 0);
	values = std::vector< std::vector<unsigned char> >(objects.size());		// Each time just checks one symbolic var.

	// Fill in exising values.
	unsigned filledNum = 0;
	int curIndex = -1;
	for (unsigned i = 0; i < objects.size(); i++) {
		bool filled = false;
		rp_dbg("objectsize %u, cItr->symVarValueMap %u\n", (unsigned)objects.size(), (unsigned)cItr->symVarValueMap.size());
		Sym_Var_To_Value_Map::iterator mapItr = cItr->symVarValueMap.begin(); 
		while (mapItr != cItr->symVarValueMap.end()) {
			char *value = mapItr->second;
			rp_dbg("SchedCache::satisfy symbolic var name object %u %s %s\n", i, mapItr->first, objects[i]->name.c_str());
			if (strcmp(mapItr->first, objects[i]->name.c_str()) == 0) {
				std::vector<unsigned char> &data = values[i];
				data.clear();

				rp_dbg("SchedCache::satisfy symbolic var name object HIT concrete cache %u %s: contains (", i, mapItr->first);
				for (unsigned j = 0; j < objects[i]->size; j++) {
					data.push_back(value[j]);
				}
				filledNum++;
				filled = true;

				// Debug.
				/*for (unsigned j = 0; j < 30; j++) {
					fprintf(stderr, "%d, ", (int)value[j]);
				}(
				fprintf(stderr, ")\n\n\n\n\n");*/
				
			}
			++mapItr;
		}
	}

	// May cover existing value, but this is fine, since this value in addr is the latest one.
	for (unsigned i = 0; i < objects.size(); i++) {
		rp_dbg("SchedCache::satisfy cmp symvar name %s %s\n", name, objects[i]->name.c_str());
		if (strcmp(name, objects[i]->name.c_str()) == 0) {
			curIndex = (int)i;
			std::vector<unsigned char> &data = values[i];
			data.clear();
			unsigned offset = 0;
			for (unsigned k = 0; k < nbytes; k++) {
				data.push_back((char)(*((long *)((long)addr + offset))));
				//fprintf(stderr, "TERN: SchedCache pushes %u for symbolic var to data offset %u\n", (char)(*((int *)((int)addr + offset))), (unsigned)data.size());
				//fflush(stderr);
				offset += 1;
			}
		}
	}

	// When filling addr for concrete value, we did not inc filledNum, this is for checking.
	/* Above is wrong, below is correct: sometimes the queried name may not exist in constraints, like "n" in LU. For this case,
		we consider that "this sym variable will not be constrained in the next trunk", then we can use this trunk.
		*/
	if (curIndex == -1) {
		rp_dbg("SchedCache::satisfy filledNum %u, objects size %u, curIndex %d, name %s\n", filledNum, (unsigned)objects.size(), curIndex, name);
		cItr->fillSymVarMap(name, addr, nbytes);
		return true;
	}
	
	if (lookupConcreteCache(cm, objects, values, cache)) {
		cItr->fillSymVarMap(name, addr, nbytes);
		return true;
	} else {
		return false;
	}
}

bool SchedCache::lookupConcreteCache(ConstraintManager *cm, std::vector<const Array*> &objects, 
	std::vector< std::vector<unsigned char> > &values, Char_Ptr_To_Int_Map &cache) {
	assert(objects.size() == values.size());
	std::vector<char> keyV;
	
	for (unsigned i = 0; i < objects.size(); i++) {
		// push magic values to seperate.
		keyV.push_back('T');
		keyV.push_back('E');
		keyV.push_back('R');
		keyV.push_back('N');

		// FIXME: FOR HTTPD, THE URL MAY HAVE CONTAINED '\0', MAKING OTHER VALUES NOT EXISTS IN THE KEY (TRUNCATE).
		std::vector<unsigned char> data = values[i];
		for (unsigned j = 0; j < data.size(); j++) {
			keyV.push_back(data[j]);
		}
	}

	char *key = new char[keyV.size() + 1];
	key[keyV.size()] = '\0';
	for (unsigned i = 0; i < keyV.size(); i++) {
		key[i] = keyV[i];
	}

	//fprintf(stderr, "lookupConcreteCache key: %s\n", key);
	if (false) {
	//if (cache.find(key) != cache.end()) {
		rp_dbg("TID %d SchedCache::lookupExprCache key match\n", gettid());
		delete key;
		return true;
	} else {
		rp_dbg("TID %d SchedCache::lookupExprCache check satisfaction\n", gettid());
		Assignment binding(objects, values);
		if (binding.satisfies(cm->begin(), cm->end())) {
			rp_dbg("TID %d SchedCache::lookupExprCache GOT satisfaction\n", gettid());
			//cache[key] = 1;
			return true;
		}
	}

	delete key;
	return false;
}




int SchedCache::countSatisfiedWithCache(CacheItr *cItr, ConstraintManager *cm, std::vector<const Array*> &objects, 
	Char_Ptr_To_Int_Map &cache, void *addr, unsigned nbytes, const char *name) {
	rp_dbg("SchedCache::satisfyWithCache\n");
	if (cm->size() == 0) {
		rp_dbg("WARN: SchedCache::satisfy, the number of constraints should be greater than 0.\n");
		cItr->fillSymVarMap(name, addr, nbytes);
		return true;
	}
	KeyType key = KeyType(cm->begin(), cm->end());
	std::vector< std::vector<unsigned char> > values;
	fillSymObjs(key, objects);
	assert(objects.size() > 0);
	values = std::vector< std::vector<unsigned char> >(objects.size());		// Each time just checks one symbolic var.

	// Fill in exising values.
	unsigned filledNum = 0;
	int curIndex = -1;
	for (unsigned i = 0; i < objects.size(); i++) {
		bool filled = false;
		rp_dbg("objectsize %u, cItr->symVarValueMap %u\n", (unsigned)objects.size(), (unsigned)cItr->symVarValueMap.size());
		Sym_Var_To_Value_Map::iterator mapItr = cItr->symVarValueMap.begin(); 
		while (mapItr != cItr->symVarValueMap.end()) {
			rp_dbg("SchedCache::satisfy symbolic var name object %u %s %s.\n", i, mapItr->first, objects[i]->name.c_str());
			if (strcmp(mapItr->first, objects[i]->name.c_str()) == 0) {
				std::vector<unsigned char> &data = values[i];
				data.clear();
				for (unsigned j = 0; j < objects[i]->size; j++) {
					char *value = mapItr->second;
					data.push_back(value[j]);
				}
				filledNum++;
				filled = true;
			}
			++mapItr;
		}
	}

	// May cover existing value, but this is fine, since this value in addr is the latest one.
	for (unsigned i = 0; i < objects.size(); i++) {
		rp_dbg("SchedCache::satisfy cmp symvar name %s %s\n", name, objects[i]->name.c_str());
		if (strcmp(name, objects[i]->name.c_str()) == 0) {
			curIndex = (int)i;
			std::vector<unsigned char> &data = values[i];
			data.clear();
			unsigned offset = 0;
			for (unsigned k = 0; k < nbytes; k++) {
				data.push_back((char)(*((long *)((long)addr + offset))));
				//fprintf(stderr, "TERN: SchedCache pushes %u for symbolic var to data offset %u\n", (char)(*((int *)((int)addr + offset))), (unsigned)data.size());
				//fflush(stderr);
				offset += 1;
			}
		}
	}

	// When filling addr for concrete value, we did not inc filledNum, this is for checking.
	/* Above is wrong, below is correct: sometimes the queried name may not exist in constraints, like "n" in LU. For this case,
		we consider that "this sym variable will not be constrained in the next trunk", then we can use this trunk.
		*/
	if (curIndex == -1) {
		fprintf(stderr, "SchedCache::satisfy filledNum %u, objects size %u, curIndex %d\n", filledNum, (unsigned)objects.size(), curIndex);
		fflush(stderr);
		cItr->fillSymVarMap(name, addr, nbytes);
		return true;
	}
	
	return countSatisfiedWithConcrete(cm, objects, values, cache);
}

int SchedCache::countSatisfiedWithConcrete(ConstraintManager *cm, std::vector<const Array*> &objects, 
	std::vector< std::vector<unsigned char> > &values, Char_Ptr_To_Int_Map &cache) {
	assert(objects.size() == values.size());
	std::vector<char> keyV;
	
	for (unsigned i = 0; i < objects.size(); i++) {
		// push magic values to seperate.
		keyV.push_back('T');
		keyV.push_back('E');
		keyV.push_back('R');
		keyV.push_back('N');

		// FIXME: FOR HTTPD, THE URL MAY HAVE CONTAINED '\0', MAKING OTHER VALUES NOT EXISTS IN THE KEY (TRUNCATE).
		std::vector<unsigned char> data = values[i];
		for (unsigned j = 0; j < data.size(); j++) {
			keyV.push_back(data[j]);
		}
	}

	char *key = new char[keyV.size() + 1];
	key[keyV.size()] = '\0';
	for (unsigned i = 0; i < keyV.size(); i++) {
		key[i] = keyV[i];
	}

        Assignment binding(objects, values);
        int count = binding.countSatisfied(cm->begin(), cm->end());
	delete key;
	return count;
}



SchedTrunk *SchedCache::queryNextTrunk(CacheItr *cItr, void *addr, unsigned nbytes, const char *name, int replayerTid) {
	if (root == NULL)
		return NULL;

	// Debug
	/*if (strstr(name, "cmdsym") || strstr(name, "sqlcmd")) {
		rp_dbg("\n\nTID %d SchedCache::query START1 with name %s, concrete bytes:", gettid(), name);
		char *p = ((char *)addr);
		for (unsigned i = 0; i < nbytes; i++) {
			rp_dbg("%d, ", (int)p[i]);
		}
		rp_dbg("\n\n\n");
	} else {
		rp_dbg("TID %d SchedCache::query START2 with name %s, concrete bytes %s\n", gettid(), name, (char *)addr);
	}*/
	
	// If it is sched track mode, the constraints have already been checked, so just return the next trunk.
/*	if (REPLAYER_USE_SCHED_TRACK) {
		unsigned nextIdx = cItr->moveOnSchedTrackTrunk();
		SchedTrunk *nextTrunk = tracks[cItr->getSchedTrackIdx()]->getTrunkAt(nextIdx);
		rp_dbg("TID %d MYTID %d move sched track trunk from %s to %s\n", gettid(), replayerTid,
			cItr->getCurTrunk()->getTidFileName().c_str(),  nextTrunk->getTidFileName().c_str());
		return nextTrunk;
	}
*/
	assert(cItr->getCurTrunk() != NULL);
	assert(cItr->getCurTrunk()->getNextNode() != NULL);
	cItr->setCurNode(cItr->getCurTrunk()->getNextNode());

	if (get_option(tern, replayer_only_one_schedule)) {
		assert(cItr->getCurNode());
		return cItr->getCurNode()->getChild(0);
	}

        // YJF
        if(get_option(tern, fuzzy_satisfy)) {

            fprintf(stderr, "fuzzy saftisfy\n\n\n");
            int total, count, max = 0, max_idx = -1;
            for(unsigned i=0; i<cItr->getCurNode()->size(); ++i) {
		SchedTrunk *st = cItr->getCurNode()->getChild(i);
                count = countSatisfiedWithCache(cItr, st->getCst(), st->getObjects(),
                                                 st->getCache(), addr, nbytes, name);
                total = st->getCst()->size();
                if(count == total) {// complete satisfaction 
                    max_idx = i;
                    break;
                }
                if(max < count) {
                    max = count;
                    max_idx = i;
                }
            }
            if(max_idx == -1)
                return NULL;
            cItr->fillSymVarMap(name, addr, nbytes);
            return cItr->getCurNode()->getChild(max_idx);
        }


	SchedTrunk *nextTrunk = NULL;

	for (unsigned i = 0; i < cItr->getCurNode()->size(); i++) {
		SchedTrunk *st = cItr->getCurNode()->getChild(i);
		rp_dbg("SchedCache::query trunk name %s, child %u(num Child %u), var name %s, symVarValueMap size %u\n", 
                       st->getTidFileName().c_str(), i, (unsigned)cItr->getCurNode()->size(), name, (unsigned)cItr->symVarValueMap.size());
		if (satisfyWithCache(cItr, st->getCst(), st->getObjects(), st->getCache(), addr, nbytes, name)) {
			nextTrunk = st;
			break;						// First hit first fit.
		}
	}

	return nextTrunk;
}

void SchedCache::dumpMemoizedSchedToDisk(int schedId, int winNum) {
	schedules[schedId]->dumpSchedTrunksToDisk(winNum);
}

unsigned SchedCache::size() {
	return schedNum;
}

bool SchedCache::simplifyExpr(MemoizedSched *ms) {
	ConstraintManager tmpCm;
	Solver::Validity result;
	int numRmvd = 0;
	
	for (unsigned i = 0; i < ms->size(); i++) {
		ConstraintManager *cm = ms->getTrunk(i)->getCst();

		while (true) {		
			int index = -1;
			bool restart = false;
			for (ConstraintManager::constraint_iterator it = cm->begin(), ie = cm->end(); it != ie; ++it) {
				ref<Expr> expr = *it;
				index++;

				// Push constraints to a tmp constraint manager.
				tmpCm.clear();
				for (ConstraintManager::constraint_iterator it2 = cm->begin(), ie2 = cm->end(); it2 != ie2; ++it2) {
					if (it != it2) {
						tmpCm.addConstraint(*it2);
					}
				}

				// Query the solver.
				bool success = false;
				result = Solver::Unknown;
				if (tmpCm.size() > 0)
					success = solver->evaluate(Query(tmpCm, expr), result);
				if (result == Solver::True) {
					numRmvd++;
					fprintf(stderr, "Expr removed, success %d, result %d, index %d, numRmvd %d, cm size %u, tmpCm size %u\n", 
						success, result, index, numRmvd, (unsigned)cm->size(), (unsigned)tmpCm.size());
					cm->erase(index);
					restart = true;
					break;
				} else {
					fprintf(stderr, "Expr NOT removed,, success %d, result %d, index %d, numRmvd %d, cm size %u, tmpCm size %u\n", 
						success, result, index, numRmvd, (unsigned)cm->size(), (unsigned)tmpCm.size());
					/*expr->print(std::cerr);
					fprintf(stderr, "\n\n=====================\n\n\n\n");*/
				}
			}

			if (!restart)
				break;


		}


	}

	return true;
}

void SchedCache::mergeSched(MemoizedSched *ms) {
	// Merge a MemoizedSched instance to current decision tree.
	bool firstTrunkAdded = false;
	int depth = 0;
	SchedTrunk *trunkItr = NULL;

	/*SchedCache::mergeSched ignores schedule due to the same cst diff sched problem.
		The cst of the first two schedules do not have expr, and the trunk size is 2. The later schdules also do not have expr in the first cst file,
		but they have a trunk size of 4. The 4 ones are major. If we merge the 2 ones into sched cache, then we can not merge the 4 ones any more. */
	if (IS_MYSQLD) { 
		// For mysqld, only pick a subset of schedules, this is due to the approximation (may have more than one sched cache root node).
		// For winsize=4, first trunk must be 4; for winsize=8, first trunk must be 8.
		if (ms->getTrunk(0)->size() != TASK_WINDOW_SIZE) {
 			fprintf(stderr, "SchedCa  e::mergeSched ignores schedule due to the same cst diff sched problem.\n");
			return;
		}
	}	

	/* This tid map maps tids from new schedule to existing schedule (i.e., newTrunk --> curTrunk).
		This tid map is used to guarantee that the tids within the sched cache is consistent. */
	int tidMap[MAX_THREAD_NUM];
	for (unsigned i = 0; i < MAX_THREAD_NUM; i++)
		tidMap[i] = -1;

	itr = root;
	if (root == NULL) {
		root = new SchedNode();
		root->addChild(ms->getTrunk(0));
		firstTrunkAdded = true;
		itr = ms->getTrunk(0)->getNextNode();
		trunkItr = ms->getTrunk(0);
		depth++;
	}

	// For each new trunk in the memoized schedule.
	for (unsigned i = 0; i < ms->size(); i++) {
		fprintf(stderr, HIGHLIGHT_STR_BEFORE);
		fprintf(stderr, "SchedCache::mergeSched 2, index %u, depth %d\n", i, depth);
		if (firstTrunkAdded) {
			firstTrunkAdded = false;
			continue;
		}
		SchedTrunk *newTrunk = ms->getTrunk(i);
		SchedTrunk *curTrunk = newTrunk;
		if (itr == NULL) {
			itr = new SchedNode();
			assert(trunkItr != NULL);
			itr->setPrevTrunk(trunkItr);
			itr->addChild(newTrunk);
			itr = newTrunk->getNextNode();
			trunkItr = newTrunk;
			depth++;
			fprintf(stderr, "SchedCache::mergeSched create new SchedNode, depth %d.\n", depth);
			continue;
		}

		bool diffCst = true;
		bool diffSched = true;

		fprintf(stderr, "SchedCache::mergeSched 3, depth %d, cur node size %u\n", depth, itr->size());
		// Use itr to traverse the current sched cache.
		for (unsigned j = 0; j < itr->size(); j++) {
			curTrunk = itr->getChild(j);
			diffSched = schedTrunkDistinct(curTrunk, newTrunk);
			bool hasCstAssert = false;
			
			if (diffSched) {
				if (IS_MYSQLD) {
					/* Heming: approaximation to solve the hidden cache problem in mysqld: if sched trunk is different, 
						then just view constraints as different, and use priority based on past finish rate to reorder the children in the parent sched node.
					*/
					hasCstAssert = true;
					diffCst = true;
				}
			}
			
			if (hasCstAssert == false) {
				diffCst = constraintsDistinct(curTrunk, newTrunk);
			}
			
			// Different constraints, diffrent sched trunks, then 'continue' and visit the next trunk of current sched node.
			if (diffCst && diffSched) {
				fprintf(stderr, "SchedCache::mergeSched 3.1, depth %d\n", depth);
				continue;
			}
	
			// Different constraints, same sched trunks. View them as different schedules.
			if (diffCst && !diffSched) {
				diffSched = true;
				fprintf(stderr, "SchedCache::mergeSched 3.2, depth %d\n", depth);
				continue;
			}
					
			// Same constraints, diffrent sched trunks.
			if (!diffCst && diffSched) {
				// This case should have been pruned by the optimizeCache() function.
				fprintf(stderr, "SchedCache::mergeSched 3.3, depth %d(%s).\n \
					THE SAME CONSTRAINTS WITH DIFFERENT SCHEDULE TRUNKS, NOT SUPPORTED BY TERN SO FAR.\n", 
					depth, curTrunk->getTidFileName().c_str());
				fprintf(stderr, "WE ONLY STOP MERGING CURRENT SCHEDULE TO THE SCHED CACHE. NO OTHER PROBLEM.\n");
				return;	
			}
		
			// Same constraints, same sched trunks. Stop looking at other siblings and go along this current branch (trunk).
			if (!diffCst && !diffSched) {
				fprintf(stderr, "SchedCache::mergeSched 3.4, depth %d\n", depth);
				// If meets tid map confliction, then just return and discard the new schedule.
				itr = curTrunk->getNextNode();
				trunkItr = curTrunk;
				depth++;
				break;
			}
		}

		/* After traversing all trunks of current node, still get different cst and different schedule trunks.
		    Then create a new path (trunk) to current sched node, and go along the new path (trunk). */
		if (diffCst && diffSched) {
			fprintf(stderr, "SchedCache::mergeSched 4, depth %d\n", depth);
			itr->addChild(newTrunk);
			curTrunk = newTrunk;
			itr = curTrunk->getNextNode();
			trunkItr = curTrunk;
		}
		fprintf(stderr, "SchedCache::mergeSched 5, depth %d\n", depth);
		fprintf(stderr, HIGHLIGHT_STR_AFTER);
	}
}

void SchedCache::loadCache() {
	// Read the ece.input.sched_cache file (tree style) and build the sched cache decision tree.
	char fileName[BASIC_SIZE] = {0};
	char inputItem[BASIC_SIZE] = {0};
	char tidFile[BASIC_SIZE] = {0};
	char cstFile[BASIC_SIZE] = {0};
	unsigned depth = 0;
	sprintf(fileName, "%s.sched_cache", INPUT);
	std::ifstream input(fileName);
	if (!input.is_open()) {
		// sched cache is empty.
		fprintf(stderr, "Sched cache is empty\n");
		return;
	}
	input.getline(inputItem, sizeof(inputItem));
	if (!input) {
		fprintf(stderr, "Error in reading from %s, please check whether it is empty. If yes, remove the whole cache and redo recording\n", fileName);
		exit(1);
	}
	sscanf(inputItem, "%u [ %s %s ]", &depth, tidFile, cstFile);
	// Jingyue: Quick hack
	if (root) {
		root = NULL;
		depth = 0;
	}
	// End Jingyue
	SchedTrunk *sc = new SchedTrunk();
	sc->loadTidsFromDisk(tidFile);
	sc->loadConstraintsFromDisk(cstFile);
	root = new SchedNode();
	root->addChild(sc);
	addSchedTrack(sc);
	loadCacheDFS(root, sc, depth, input, 0);
	input.close();
}

void SchedCache::loadCacheDFS(SchedNode *node, SchedTrunk *curTrunk, unsigned &depth, std::ifstream &input, int callSite) {
	fprintf(stderr, "SchedCache::loadCacheDFS\n");
	char inputItem[BASIC_SIZE] = {0};
	char tidFile[BASIC_SIZE] = {0};
	char cstFile[BASIC_SIZE] = {0};
	unsigned nextDepth = 0;
	if (node == NULL) {
		return;
	}
	fprintf(stderr, "SchedCache::loadCacheDFS1\n");
	streampos curPos = input.tellg();
	input.getline(inputItem, sizeof(inputItem));
	if (input.eof())															// should do the eof check after a read operation, not check eof and then read.
		return;
	fprintf(stderr, "SchedCache::loadCacheDFS2\n");
	sscanf(inputItem, "%u [ %s %s ]", &nextDepth, tidFile, cstFile);
	fprintf(stderr, "SchedCache::loadCacheDFS3, nextDepth %u\n", nextDepth);
	SchedTrunk *sc = new SchedTrunk();
	fprintf(stderr, "SchedCache::loadCacheDFS4, %s %s\n", tidFile, cstFile);
	sc->loadTidsFromDisk(tidFile);
	sc->loadConstraintsFromDisk(cstFile);

	rp_dbg("SchedCache::loadCacheDFS(%d) node %p, curTrunk %s depth %u, nextDepth %u\n", 
		callSite, (void *)node, curTrunk->getTidFileName().c_str(), depth, nextDepth);
	
	if (depth < nextDepth) {
		// Expand on curTrunk
		SchedNode *nextNode = curTrunk->getNextNode();
		if (nextNode == NULL) {
			 nextNode = new SchedNode();
			 curTrunk->setNextNode(nextNode);
		}
		nextNode->addChild(sc);
		addSchedTrack(sc);
		rp_dbg("loadCacheDFS1 add child %s to node %p, depth %u, nextDepth %u\n", sc->getTidFileName().c_str(), (void *)nextNode, depth, nextDepth);
		depth = nextDepth;
		loadCacheDFS(nextNode, sc, depth, input, 1);			// DFS. Go along "nextNode".
	} 
	// If nextDepth, the next line depth, equals to or smaller than the current "depth", this mean we have hit a leaf of the sched cache, 
	// then it is time to build the sched track for this schedule.
	else if (depth == nextDepth) {
		// Append to current node.
		node->addChild(sc);
		addSchedTrack(sc);
		rp_dbg("loadCacheDFS2 add child %s to node %p, depth %u, nextDepth %u\n", sc->getTidFileName().c_str(), (void *)node, depth, nextDepth);
		loadCacheDFS(node, sc, depth, input, 2);					// update "curTrunk" to "sc" and then move on.
	} else {																				// backtrack both the decision tree and the input stream.
		rp_dbg("loadCacheDFS3 depth %u, nextDepth %u, curNode %p, curTrunk %p(%s), prevNode %p\n", 
			depth, nextDepth, (void *)node, (void *)sc, sc->getTidFileName().c_str(), (void *)sc->getPrevNode());
		depth--;
		SchedNode *backTrackNode = node->getPrevTrunk()->getPrevNode();
		SchedTrunk *backTrackTrunk = node->getPrevTrunk();
		delete sc;			// sc is uesless at this case.
		input.seekg(curPos);
		loadCacheDFS(backTrackNode, backTrackTrunk, depth, input, 3);
	}
}

void SchedCache::createMemoizedSched() {
	schedules[schedNum] = new MemoizedSched();
}

// Dump memoized sched trunks to disk and merge current trunks to root.
void SchedCache::dumpMemoizedSched(int winNum) {
	if (MEMOIZER_SIMPLIFY_EXPR)
		simplifyExpr(schedules[schedNum]);

	// Must run mergeSched() first and then dumpMemoizedSchedToDisk(), since mergeSched() would update tids in the memoized schedules.
	if (!IS_BATCH_PROGRAM)
		schedules[schedNum]->normalize();
	mergeSched(schedules[schedNum]);
	dumpMemoizedSchedToDisk(schedNum, winNum);

	SchedTrunk *sc = schedules[schedNum]->getTrunk(schedules[schedNum]->size()-1);
	fprintf(stderr, "%s: number of schedules %d, number of trunks in the latest schedule %u, number of ops in the latest trunks %u, \
		number of constraints at the 0 th track of this trunk %u\n", 
		END_TASK_LANDMARK, schedNum+1, schedules[schedNum]->size(), sc->size(), sc->constraintSize(0));
	schedNum++;
}

void SchedCache::storeCache(int winNum) {
	char fileName[BASIC_SIZE] = {0};
	sprintf(fileName, "%s.sched_cache", INPUT);
	std::ofstream output(fileName);
	fprintf(stderr, "SchedCache::storeCache\n");
	dumpMemoizedSched(winNum);										// Here we have merged schedules.
	storeCacheDFS(root, 0, output);
	output.flush();
	output.close();
	fprintf(stderr, "Finished storeCache\n");
}

void SchedCache::storeCacheDFS(SchedNode *node, unsigned depth, std::ofstream &output) {
	//fprintf(stderr, "SchedCache::storeCacheDFS depth %u, node %p, ", depth, (void *)node);
	char blanks[BASIC_SIZE];
	unsigned offset = 0;
	if (node == NULL) {
		fprintf(stderr, "\n");
		return;
	}

	//fprintf(stderr, "node size %u.\n", node->size());
	for (unsigned i = 0; i < node->size(); i++) {
		memset(blanks, 0, sizeof(blanks));
		offset = 0;
		for (unsigned k = 0; k < depth; k++) {
			offset += sprintf(blanks + offset, "	");
		}
		SchedTrunk *sc = node->getChild(i);
		//std::cerr << blanks << "Depth: " << depth << ", " << i << ", " << node->size() << " [" << sc->getTidFileName() << " " << sc->getCstFileName() << "]\n";
		output << blanks << depth << " [ " << sc->getTidFileName() << " " << sc->getCstFileName() << " ]\n";
		storeCacheDFS(sc->getNextNode(), depth + 1, output);
	}
}

void SchedCache::optimizeCache() {
	// Optimize the cache to remove redundancy.
	// TO DO.
	
}

SchedNode *SchedCache::getRoot() {
	return root;
}

void SchedCache::fillSymObjs(KeyType &key, std::vector<const Array*> &objects) {
	Char_Ptr_To_Int_Map symVars;

	symVars.clear();
	KeyType::iterator itrStart = key.begin();
	KeyType::iterator itrEnd = key.begin();
	itrEnd++;

	

	if (objects.size() == 0) {
		if (!IS_MYSQLD) {
			findSymbolicObjects(key.begin(), key.end(), objects);
			return;
		}

		// Opt for mysqld since there are too many expr in one trunk. More than 1000.
		do {
			std::vector<const Array*> tmpObjects;
			tmpObjects.clear();
			findSymbolicObjects(itrStart, itrEnd, tmpObjects);
			for (unsigned i = 0; i < tmpObjects.size(); i++) {
				if (symVars.find(tmpObjects[i]->name.c_str()) == symVars.end()) {
					objects.push_back(tmpObjects[i]);
					symVars[tmpObjects[i]->name.c_str()] = 1;
				}
			}
			
			if (objects.size() == TASK_WINDOW_SIZE)
				break;

			itrStart++;
			if (itrStart == key.end())
				break;
			itrEnd++;
		} while (1);
	}
}

bool SchedCache::constraintsDistinctWithObjects(ConstraintManager *cm1, std::vector<const Array*> &objects1, 
	ConstraintManager *cm2, std::vector<const Array*> &objects2) {
	//return true;
	// FIXME: SOLVER IS NOT WORKING DUE TO SOME UNKNOWN REASONS, 
	// SO TEMPORARILY I ONLY USE THE CONSTRAINT SIZE TO DISTINCT THEM.
	bool result = false;
	fprintf(stderr, "SchedCache::constraintsDistinct start\n");
	if (cm1->size() == cm2->size() && cm1->size() == 0)
		return false;
	if (cm1->size() != cm2->size() && (cm1->size() == 0 || cm2->size() == 0 ))
		return true;

	//printCst(cm1);
	//printCst(cm2);

	KeyType key1 = KeyType(cm1->begin(), cm1->end());
	KeyType key2 = KeyType(cm2->begin(), cm2->end());
	fprintf(stderr, "SchedCache::constraintsDistinct findSymbolicObjects\n");
	fillSymObjs(key1, objects1);
	fillSymObjs(key2, objects2);
	// Do some simple checks before consulting the solver.
	if (objects1.size() != objects2.size())
		return true;			

	/* This is the key point to solve the solver problem: actually, an expression stores an Array instance.
	     Although two expressions are the same in grammar, their Array instance may not be the same,
	     then the solve will treat them as two symbolic variables.
	     My method to fix the problem is addint a Eq expression for the two symbolic variables to build their relationship. */
	//assert(objects1.size() == objects2.size() && objects1.size() == 1);

	// TEMP
	if (objects1.size() != objects2.size())
		return true;

	fprintf(stderr, "SchedCache::constraintsDistinct preprocess expr\n");
	ConstraintManager *cm = new ConstraintManager();
	for (unsigned i = 0; i < objects1.size(); i++) {
		for (unsigned j = 0; j < objects2.size(); j++) {
			if (objects1[i]->name == objects2[j]->name) {
				assert(objects1[i]->size == objects2[j]->size);
				for (unsigned k = 0; k < objects1[i]->size; k++) {
					cm->addConstraint(EqExpr::create(
						ReadExpr::create(UpdateList(objects1[i], 0), ConstantExpr::alloc(k, Expr::Int32)),
						ReadExpr::create(UpdateList(objects2[j], 0), ConstantExpr::alloc(k, Expr::Int32))));
				}
			}
		}
	}

	fprintf(stderr, "SchedCache::constraintsDistinct preprocess expr2\n");
	ref<Expr> e1 = ConstantExpr::alloc(1, Expr::Bool);
	ref<Expr> e2 = ConstantExpr::alloc(1, Expr::Bool);
	for (ConstraintManager::constraint_iterator it = cm1->begin(), ie = cm1->end(); it != ie; ++it) {
		ref<Expr> ce = *it;
		e1 = AndExpr::create(e1, ce);
	}
	for (ConstraintManager::constraint_iterator it = cm2->begin(), ie = cm2->end(); it != ie; ++it) {
		ref<Expr> ce = *it;
		e2 = AndExpr::create(e2, ce);
	}
	fprintf(stderr, "SchedCache::constraintsDistinct preprocess expr3\n");
	e2 = Expr::createIsZero(e2);
	e1 = AndExpr::create(e1, e2);
	cm->addConstraint(e1);
	fprintf(stderr, "SchedCache::constraintsDistinct preprocess expr4\n");
	result = solve(cm);
	delete cm;
	
	return result;
}

bool SchedCache::constraintsDistinct(SchedTrunk *tr1, SchedTrunk *tr2) {	
	ConstraintManager *cm1 = tr1->getCst();
	ConstraintManager *cm2 = tr2->getCst();
	return constraintsDistinctWithObjects(cm1, tr1->getObjects(), cm2, tr2->getObjects());
}

bool SchedCache::schedTrunkDistinct(SchedTrunk *tr1, SchedTrunk *tr2) {
	char tidInfo1[BASIC_SIZE];
	char tidInfo2[BASIC_SIZE];
	
	if (tr1->size() != tr2->size()) {
		fprintf(stderr, "Distinct trunk size %u and %u\n", tr1->size(), tr2->size());
		return true;
	}
	for (unsigned i = 0; i < tr1->size(); i++) {
		memset(tidInfo1, 0, BASIC_SIZE);
		memset(tidInfo2, 0, BASIC_SIZE);
		strcpy(tidInfo1, tr1->tidInfoAt(i));
		strcpy(tidInfo2, tr2->tidInfoAt(i));
		
		// Compare landmark type.
		if (tr1->opAt(i) != tr2->opAt(i)) {
			fprintf(stderr, "WARN: Distinct trunk OP at offset %u (%s) and (%s)\n", i, tr1->tidInfoAt(i), tr2->tidInfoAt(i));
			/* Since pbzip2 has usleep() in fileWriter, which makes the recorded schedule non-deterministic,
				but as long as we recorde this schedule, we can replay it, so the non-deter recorded schedule is not a problem in replay.
				However, if the schedule trunk is non-deter, which could perturb the schedule merging phase, so I relax the schedule trunk
				requirement for batch program (and this non determinism only happens in pbzip2 in our batch programs).
			*/
			if (!IS_BATCH_PROGRAM) {
				return true;
			}
		}

		if (tr1->tidAt(i) != tr2->tidAt(i)) {
			fprintf(stderr, "WARN: Distinct trunk ID at offset %u (%s) and (%s)\n", i, tr1->tidInfoAt(i), tr2->tidInfoAt(i));
			if (!IS_BATCH_PROGRAM) {
				return true;
			}
		}
	}

	return false;
}

void SchedCache::printSchedTrunk(SchedTrunk *tr) {
	fprintf(stderr, "TidFileName: %s\n", tr->getTidFileName().c_str());
	for (unsigned i = 0; i < tr->size(); i++) {
		fprintf(stderr, "[%u]: %s\n", i, tr->tidInfoAt(i));
	}
	fprintf(stderr, "\n\n");
	fflush(stderr);
}

bool SchedCache::solve(ConstraintManager *cm) {
	/*for (ConstraintManager::constraint_iterator it = cm->begin(), ie = cm->end(); it != ie; ++it) {
		ref<Expr> ce = *it;
		ce->print(std::cerr);
		fprintf(stderr, "\n\n----------------------------------\n\n");
	}*/
	fprintf(stderr, "SchedCache::solve, please wait...\n");
	KeyType key = KeyType(cm->begin(), cm->end());
	std::vector<const Array*> objects;
	std::vector< std::vector<unsigned char> > values;
	findSymbolicObjects(key.begin(), key.end(), objects);
	/*for (unsigned i = 0; i < objects.size(); i++) {
		fprintf(stderr, "Object %p [%u] name: %s.\n", (void *)objects[i], i, objects[i]->name.c_str());
	}*/
	values.clear();
	bool success = solver->getInitialValues(Query(*cm, ConstantExpr::alloc(0, Expr::Bool)), objects, values);
	fprintf(stderr, "Constraints size (%u), success %d, values size %u.\n", 
		(unsigned)cm->size(), success, (unsigned)values.size());
	/*if (values.size() > 0) {
		for (unsigned i = 0; i < values.size(); i++) {
			std::vector<unsigned char> &data = values[i];
			for (unsigned j = 0; j < data.size(); j++) {
				fprintf(stderr, "values[%u][%u] = %u\n", i, j, (unsigned)data[j]);
			}
		}
	}*/

	return success;
}

void SchedCache::printCst(ConstraintManager *cm) {
	fprintf(stderr, "\n\n============================\n\n");
	for (ConstraintManager::constraint_iterator it = cm->begin(), ie = cm->end(); it != ie; ++it) {
		ref<Expr> ce = *it;
		ce->print(std::cerr);
		fprintf(stderr, "\n\n----------------------------------\n\n");
	}
}

int SchedCache::addTid(char *tidInfo) {
	return schedules[schedNum]->addTid(tidInfo);
}

int SchedCache::addConstraint(unsigned trackId, ref<Expr> expr) {
	/*fprintf(stderr, HIGHLIGHT_STR_BEFORE);
	expr->print(std::cerr);
	fprintf(stderr, HIGHLIGHT_STR_AFTER);*/
	return schedules[schedNum]->addConstraint(trackId, expr);
}

void SchedCache::addSymVar(const Array *arr) {
	schedules[schedNum]->addSymVar(arr);
}

// This function is called within update region, i.e., within the markBroken() function in replayer.
void SchedCache::adjustPriority(SchedTrunk *curTrunk, unsigned curTrackIndex, int brokenReason) {
	SchedNode *prevNode = curTrunk->getPrevNode();
	// brokenReason == 2 means "no schedule".
	if (/*brokenReason != 2 && */prevNode->size() > 1) {
		/* Aproximation for mysqld, update the order of the prev node of current trunk.
			Only Update the current trunk. For former trunk, we do not need to do the reorder update, because they have been successfully finished.
		*/
		unsigned i = 0;
		for (i = 0; i < prevNode->size(); i++) {
			if (prevNode->getChild(i) == curTrunk) {
				rp_dbg("Reorder trunk %p, index %u at sched node %p, since this trunk is broken\n", (void *)curTrunk, i, (void *)prevNode);
				break;
			}
		}
		assert(i < prevNode->size());
		prevNode->delChild(i);
		prevNode->addChild(curTrunk);

		if (REPLAYER_USE_SCHED_TRACK) {
			// Adjust priority of tracks. Change the order.
			std::vector<unsigned> tracks = getRoot()->getChild(0)->getEnabledTracks();
			assert(TernUtil::elementNotInVector(tracks, curTrackIndex));
			TernUtil::delElementFromVector(tracks, curTrackIndex);
			tracks.push_back(curTrackIndex);
		}
		
		// Debug utility.
		/*for (i = 0; i < prevNode->size(); i++) {
			rp_dbg("New trunk %p (%s), index %u at sched node %p\n", 
				(void *)prevNode->getChild(i), prevNode->getChild(i)->getTidFileName().c_str(), i, (void *)prevNode);
		}*/
	}
}

// This function is called after each node->addChild() function in loading sched cache.
void SchedCache::addSchedTrack(SchedTrunk *curTrunk) {
		if (REPLAYER_USE_SCHED_TRACK && IS_MYSQLD && curTrunk->isLeafTrunk()) {
			SchedTrack *newSchedTrack = new SchedTrack(curTrunk->getTidFileName().c_str(), NULL, numTracks);
			fprintf(stderr, "SchedCache::addSchedTrack before\n");
			newSchedTrack->buildTrack(curTrunk, root); 
			tracks.push_back(newSchedTrack);
			numTracks++;
			fprintf(stderr, "SchedCache::addSchedTrack\n");
		}
}

SchedTrack *SchedCache::getTrackByIndex(unsigned index) {
	assert(index < tracks.size());
	return tracks[index];
}

void SchedCache::delRPTidFromAllTracks(int replayTid) {
	for (unsigned i = 0; i < tracks.size(); i++) {
		tracks[i]->delTid(replayTid);
	}
}

